Definitions | P Q, A, b, x:AB(x), int_seg(i; j), x:A. B(x), t T, #$n, i z j, tt, ff, sqequal(s; t), sq_type(T), guard(T), SqStable(P), rps(x; y), P Q, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), if a=b then c else d, left + right, Unit, P Q, x:A B(x), P Q, T, a < b, s = t, b, i <z j, True, prop{i:l}, Type, , , lelt(i; j; k), A B, P Q, False, void, bor(p; q), band(p; q), (i = j), {x:A| B(x)} |